grammar AlloyANTLR4Grammar;

// rules
specification           : module? open* paragraph* EOF;
module                  : MODULE_KEYWORD name (LSQRBRACKET (EXACTLY_KEYWORD)? name (COMMA (EXACTLY_KEYWORD)? name)* RSQRBRACKET)?; 
open                    : PRIVATE_KEYWORD? OPEN_KEYWORD name (LSQRBRACKET ref (COMMA ref)* RSQRBRACKET)? AS_KEYWORD name;
paragraph               : factDecl | assertDecl | funDecl | cmdDecl | enumDecl | sigDecl;
factDecl                : FACT_KEYWORD name? block;
assertDecl              : ASSERT_KEYWORD name? block;
funDecl                 : PRIVATE_KEYWORD? FUN_KEYWORD (ref PERIOD)? name ((LPARENTHESIS decl* RPARENTHESIS COLON) | (LSQRBRACKET decl* RSQRBRACKET COLON))? exprH block
                        | PRIVATE_KEYWORD? PRED_KEYWORD (ref PERIOD)? name ((LPARENTHESIS decl* RPARENTHESIS COLON) | (LSQRBRACKET decl* RSQRBRACKET COLON))? block;
cmdDecl                 : (name COLON)? (RUN_KEYWORD | CHECK_KEYWORD)? (name | block)? scope;
scope                   : FOR_KEYWORD ((NUMBER (BUT_KEYWORD typescope (COMMA typescope)*)?) | (typescope (COMMA typescope)*));
typescope               : EXACTLY_KEYWORD? NUMBER (name | (INT_KEYWORD | SEQINT_KEYWORD))?;
sigDecl                 : sigQual* SIG_KEYWORD name (COMMA name)* sigExt? LCRLBRACKET decl* RCRLBRACKET block?;
enumDecl                : ENUM_KEYWORD name LCRLBRACKET name (COMMA name)* RCRLBRACKET;
sigQual                 : ABSTRACT_KEYWORD | LONE_KEYWORD | ONE_KEYWORD | SOME_KEYWORD | PRIVATE_KEYWORD;
sigExt                  : EXTENDS_KEYWORD ref
                        | IN_KEYWORD ref (PLUS ref)*;
exprH                   : LCRLBRACKET decl (COMMA decl)* blockOrBar RCRLBRACKET exprT
                        | block exprT
                        | AT? name exprT
                        | LPARENTHESIS exprH RPARENTHESIS exprT
                        | SEQINT_KEYWORD exprT
                        | INT_KEYWORD exprT
                        | UNIV_KEYWORD exprT
                        | IDEN_KEYWORD exprT
                        | NONE_KEYWORD exprT
                        | MINUS NUMBER exprT
                        | NUMBER exprT
                        | LET_KEYWORD letDecl (COMMA letDecl)* blockOrBar exprT
                        | quant decl (COMMA decl)* blockOrBar exprT
                        | unOp exprH exprT;
exprT                   : binOp exprH exprT
                        | arrowOp exprH exprT
                        | (EXCLAMATION | NOT_KEYWORD)? compareOp exprH exprT
                        | IMPLICATION_KEYWORD? exprH ELSE_KEYWORD exprH exprT
                        | LSQRBRACKET exprH (COMMA exprH)* RSQRBRACKET exprT
                        | ;//epsilon
decl                    : PRIVATE_KEYWORD? DISJ_KEYWORD? name (COMMA name)* COLON DISJ_KEYWORD? exprH;
letDecl                 : name EQUALS exprH;
quant                   : ALL_KEYWORD | NO_KEYWORD | SOME_KEYWORD | LONE_KEYWORD | ONE_KEYWORD | SUM_KEYWORD;
binOp                   : DISJUNCTION_KEYWORD | OR_KEYWORD | CONJUNCTION_KEYWORD | AND_KEYWORD | ET | BI_IMPLIC_KEYWORD | IFF_KEYWORD | IMPLICATION_KEYWORD | PLUS | MINUS | OVERRIDE_KEYWORD | RESTRICTION_KEYWORD | PERIOD | R2_ARROWS_KEYWORD | R3_ARROWS_KEYWORD | L2_ARROWS_KEYWORD;
arrowOp                 : (SOME_KEYWORD | ONE_KEYWORD | LONE_KEYWORD | SET_KEYWORD)? RARROW_KEYWORD (SOME_KEYWORD | ONE_KEYWORD | LONE_KEYWORD | SET_KEYWORD)?;
compareOp               : EQUALS | IN_KEYWORD | GT_KEYWORD | GET_KEYWORD | LT_KEYWORD | ELT_KEYWORD;
unOp                    : EXCLAMATION | NOT_KEYWORD | NO_KEYWORD | SOME_KEYWORD | LONE_KEYWORD | ONE_KEYWORD | SET_KEYWORD | SEQ_KEYWORD | HASH | TILDE | ASTERIX | CARET;
block                   : LCRLBRACKET exprH* RCRLBRACKET;
blockOrBar              : block
                        | BAR exprH;
name                    : (THIS_KEYWORD | NAME) (SLASH NAME)*;
ref                     : name | (UNIV_KEYWORD | INT_KEYWORD | SEQINT_KEYWORD);

// literals
NAME                    : [a-zA-Z][a-zA-Z0-9"'_]*;
NUMBER                  : [0-9]+;
COMMA                   : ',';
PLUS                    : '+';
EQUALS                  : '=';
MINUS                   : '-';
PERIOD                  : '.';
COLON                   : ':';
SLASH                   : '/';
LSQRBRACKET             : '[';
RSQRBRACKET             : ']';
LCRLBRACKET             : '{';
RCRLBRACKET             : '}';
LPARENTHESIS            : '(';
RPARENTHESIS            : ')';
AT                      : '@';
ET                      : '&';
EXCLAMATION             : '!';
HASH                    : '#';
TILDE                   : '~';
ASTERIX                 : '*';
CARET                   : '^';
BAR                     : '|';
    // keywords
EXACTLY_KEYWORD     : 'exactly';
MODULE_KEYWORD      : 'module';
THIS_KEYWORD        : 'this';
PRIVATE_KEYWORD     : 'private';
OPEN_KEYWORD        : 'open';
AS_KEYWORD          : 'as';
UNIV_KEYWORD        : 'univ';
INT_KEYWORD         : 'Int';
SEQINT_KEYWORD      : 'seq/Int';
SEQ_KEYWORD         : 'seq';
FACT_KEYWORD        : 'fact';
ASSERT_KEYWORD      : 'assert';
FUN_KEYWORD         : 'fun';
PRED_KEYWORD        : 'pred';
RUN_KEYWORD         : 'run';
CHECK_KEYWORD       : 'check';
FOR_KEYWORD         : 'for';
BUT_KEYWORD         : 'but';
SIG_KEYWORD         : 'sig';
ENUM_KEYWORD        : 'enum';
ABSTRACT_KEYWORD    : 'abstract';
LONE_KEYWORD        : 'lone';
ONE_KEYWORD         : 'one';
SOME_KEYWORD        : 'some';
EXTENDS_KEYWORD     : 'extends';
IN_KEYWORD          : 'in';
NONE_KEYWORD        : 'none';
IDEN_KEYWORD        : 'iden';
IMPLICATION_KEYWORD : '=>' | 'implies';
ELSE_KEYWORD        : 'else';
NOT_KEYWORD         : 'not' | '!';
LET_KEYWORD         : 'let';
DISJ_KEYWORD        : 'disj';
ALL_KEYWORD         : 'all';
NO_KEYWORD          : 'no';
SET_KEYWORD         : 'set';
SUM_KEYWORD         : 'sum';
AND_KEYWORD         : 'and';
CONJUNCTION_KEYWORD : '&&';
OR_KEYWORD          : 'or';
DISJUNCTION_KEYWORD : '||';
IFF_KEYWORD         : 'iff';
BI_IMPLIC_KEYWORD   : '<=>';
OVERRIDE_KEYWORD    : '++';
RESTRICTION_KEYWORD : '<:' | ':>';
R2_ARROWS_KEYWORD   : '>>';
R3_ARROWS_KEYWORD   : '>>>';
L2_ARROWS_KEYWORD   : '<<';
RARROW_KEYWORD      : '->';
GT_KEYWORD          : '>';
GET_KEYWORD         : '>=';
LT_KEYWORD          : '<';
ELT_KEYWORD         : '=<';
    
//WS     : [ \t\n\r]+ -> skip ;